Nuprl Definition : scheme-compatible 11,40

scheme-compatible(A;B)
== let na,La,Ra = A in 
== let nb,Lb,Rb = B in 
== nmr_a:Namer(na;La), nmr_b:Namer(nb;Lb).
== namer-disjoint(na;nb;nmr_a;nmr_b)  Ra(nmr_a) || Rb(nmr_b) 
latex



clarification:

scheme-compatible{i:l}
scheme-compatible(A; B)
== let na,La,Ra = A in 
== let nb,Lb,Rb = B in 
== nmr_a:Namer(na;La), nmr_b:Namer(nb;Lb).
== namer-disjoint(na;nb;nmr_a;nmr_b)  R-compat{i:l}((Ra(nmr_a)); (Rb(nmr_b))) 
latex


Definitionslet x,y,z = a in t(x;y;z), x:A. B(x), Namer(n;Id_list), P  Q, A || B, f(a)
FDL editor aliasesscheme-compatible

origin